class Choicepoint {
    Stack<Conjunct> query;
    Stack<Variable> bindings;
    boolean finished;
    
    public Choicepoint(Stack<Conjunct> query,
                       Stack<Variable> bindings,
                       boolean finished) {
        this.query = query;
        this.bindings = bindings;
        this.finished = finished;
    }
    
    public Choicepoint(Conjunct... query) {
        this.query = null;
        this.bindings = null;
        this.finished = false;
        
        for(int i = query.length - 1; i >= 0; i--) {
            this.query = new Stack<Conjunct>(query[i],this.query);
        }
    }
    
    public void undoBindings() {
        while(bindings != null) {
            bindings.head.unbind();
            bindings = bindings.tail;
        }
    }
    
    public Choicepoint withIncrementedChoice() {
        return new Choicepoint
            (new Stack<Conjunct>(query.head.withIncrementedChoice(),
                                 query.tail),
             bindings,
             finished);
    }
    
    public static Stack<Choicepoint> push(Stack<Choicepoint> stack, Stack<Variable> bindings,
                                          Term... terms) { // UNROLL THIS LOOP
        Stack<Conjunct> query = stack.head.query.tail;
        for(int i = terms.length-1; i >= 0; i--) {
            query = new Stack<Conjunct>(new Predicate(terms[i],0,stack.height+1),query);
        }
        return new Stack<Choicepoint>(new Choicepoint(query,bindings,false),stack);
    }
    
    public static Stack<Choicepoint> compact(Stack<Choicepoint> stack) {
        stack.tail.head.query = stack.head.query;
        stack.tail.head.bindings = Stack.append(stack.tail.head.bindings,stack.head.bindings);
        return stack.tail;
    }
}
